thus A1: 36 = ((2 * 2) * 3) * 3 ; :: thesis: 36 has_exactly_two_different_prime_divisors
take P2 ; :: according to NUMBER07:def 4 :: thesis: ex q being Prime st
( P2 <> q & P2 divides 36 & q divides 36 & ( for r being Prime st r <> P2 & r <> q holds
not r divides 36 ) )
take P3 ; :: thesis: ( P2 <> P3 & P2 divides 36 & P3 divides 36 & ( for r being Prime st r <> P2 & r <> P3 holds
not r divides 36 ) )
thus P2 <> P3 ; :: thesis: ( P2 divides 36 & P3 divides 36 & ( for r being Prime st r <> P2 & r <> P3 holds
not r divides 36 ) )
((2 * 2) * 3) * 3 = 2 * ((2 * 3) * 3) ;
hence P2 divides 36 ; :: thesis: ( P3 divides 36 & ( for r being Prime st r <> P2 & r <> P3 holds
not r divides 36 ) )
thus P3 divides 36 by A1; :: thesis: for r being Prime st r <> P2 & r <> P3 holds
not r divides 36
let r be Prime; :: thesis: ( r <> P2 & r <> P3 implies not r divides 36 )
assume A2: ( r <> P2 & r <> P3 ) ; :: thesis: not r divides 36
assume r divides 36 ; :: thesis: contradiction
then ( r = 1 or r = 2 or r = 3 or r = 4 or r = 6 or r = 9 or r = 12 or r = 18 or r = 36 ) by Th15;
then ( r = 2 or r = 3 ) by INT_2:def 4, XPRIMES0:4, XPRIMES0:6, XPRIMES0:9, XPRIMES0:12, XPRIMES0:18, XPRIMES0:36;
hence contradiction by A2; :: thesis: verum