Metamath Proof Explorer

Theorem 2sqlem6

Description: Lemma for 2sq . If a number that is a sum of two squares is divisible by a number whose prime divisors are all sums of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem6.1 
|- ( ph -> A e. NN )
2sqlem6.2 
|- ( ph -> B e. NN )
2sqlem6.3 
|- ( ph -> A. p e. Prime ( p || B -> p e. S ) )
2sqlem6.4 
|- ( ph -> ( A x. B ) e. S )
Assertion 2sqlem6 
|- ( ph -> A e. S )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 2sqlem6.1 
 |-  ( ph -> A e. NN )
3 2sqlem6.2 
 |-  ( ph -> B e. NN )
4 2sqlem6.3 
 |-  ( ph -> A. p e. Prime ( p || B -> p e. S ) )
5 2sqlem6.4 
 |-  ( ph -> ( A x. B ) e. S )
6 breq2 
 |-  ( x = 1 -> ( p || x <-> p || 1 ) )
7 6 imbi1d 
 |-  ( x = 1 -> ( ( p || x -> p e. S ) <-> ( p || 1 -> p e. S ) ) )
8 7 ralbidv 
 |-  ( x = 1 -> ( A. p e. Prime ( p || x -> p e. S ) <-> A. p e. Prime ( p || 1 -> p e. S ) ) )
9 oveq2 
 |-  ( x = 1 -> ( m x. x ) = ( m x. 1 ) )
10 9 eleq1d 
 |-  ( x = 1 -> ( ( m x. x ) e. S <-> ( m x. 1 ) e. S ) )
11 10 imbi1d 
 |-  ( x = 1 -> ( ( ( m x. x ) e. S -> m e. S ) <-> ( ( m x. 1 ) e. S -> m e. S ) ) )
12 11 ralbidv 
 |-  ( x = 1 -> ( A. m e. NN ( ( m x. x ) e. S -> m e. S ) <-> A. m e. NN ( ( m x. 1 ) e. S -> m e. S ) ) )
13 8 12 imbi12d 
 |-  ( x = 1 -> ( ( A. p e. Prime ( p || x -> p e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) <-> ( A. p e. Prime ( p || 1 -> p e. S ) -> A. m e. NN ( ( m x. 1 ) e. S -> m e. S ) ) ) )
14 breq2 
 |-  ( x = y -> ( p || x <-> p || y ) )
15 14 imbi1d 
 |-  ( x = y -> ( ( p || x -> p e. S ) <-> ( p || y -> p e. S ) ) )
16 15 ralbidv 
 |-  ( x = y -> ( A. p e. Prime ( p || x -> p e. S ) <-> A. p e. Prime ( p || y -> p e. S ) ) )
17 oveq2 
 |-  ( x = y -> ( m x. x ) = ( m x. y ) )
18 17 eleq1d 
 |-  ( x = y -> ( ( m x. x ) e. S <-> ( m x. y ) e. S ) )
19 18 imbi1d 
 |-  ( x = y -> ( ( ( m x. x ) e. S -> m e. S ) <-> ( ( m x. y ) e. S -> m e. S ) ) )
20 19 ralbidv 
 |-  ( x = y -> ( A. m e. NN ( ( m x. x ) e. S -> m e. S ) <-> A. m e. NN ( ( m x. y ) e. S -> m e. S ) ) )
21 16 20 imbi12d 
 |-  ( x = y -> ( ( A. p e. Prime ( p || x -> p e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) <-> ( A. p e. Prime ( p || y -> p e. S ) -> A. m e. NN ( ( m x. y ) e. S -> m e. S ) ) ) )
22 breq2 
 |-  ( x = z -> ( p || x <-> p || z ) )
23 22 imbi1d 
 |-  ( x = z -> ( ( p || x -> p e. S ) <-> ( p || z -> p e. S ) ) )
24 23 ralbidv 
 |-  ( x = z -> ( A. p e. Prime ( p || x -> p e. S ) <-> A. p e. Prime ( p || z -> p e. S ) ) )
25 oveq2 
 |-  ( x = z -> ( m x. x ) = ( m x. z ) )
26 25 eleq1d 
 |-  ( x = z -> ( ( m x. x ) e. S <-> ( m x. z ) e. S ) )
27 26 imbi1d 
 |-  ( x = z -> ( ( ( m x. x ) e. S -> m e. S ) <-> ( ( m x. z ) e. S -> m e. S ) ) )
28 27 ralbidv 
 |-  ( x = z -> ( A. m e. NN ( ( m x. x ) e. S -> m e. S ) <-> A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) )
29 24 28 imbi12d 
 |-  ( x = z -> ( ( A. p e. Prime ( p || x -> p e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) <-> ( A. p e. Prime ( p || z -> p e. S ) -> A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) ) )
30 breq2 
 |-  ( x = ( y x. z ) -> ( p || x <-> p || ( y x. z ) ) )
31 30 imbi1d 
 |-  ( x = ( y x. z ) -> ( ( p || x -> p e. S ) <-> ( p || ( y x. z ) -> p e. S ) ) )
32 31 ralbidv 
 |-  ( x = ( y x. z ) -> ( A. p e. Prime ( p || x -> p e. S ) <-> A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) )
33 oveq2 
 |-  ( x = ( y x. z ) -> ( m x. x ) = ( m x. ( y x. z ) ) )
34 33 eleq1d 
 |-  ( x = ( y x. z ) -> ( ( m x. x ) e. S <-> ( m x. ( y x. z ) ) e. S ) )
35 34 imbi1d 
 |-  ( x = ( y x. z ) -> ( ( ( m x. x ) e. S -> m e. S ) <-> ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) )
36 35 ralbidv 
 |-  ( x = ( y x. z ) -> ( A. m e. NN ( ( m x. x ) e. S -> m e. S ) <-> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) )
37 32 36 imbi12d 
 |-  ( x = ( y x. z ) -> ( ( A. p e. Prime ( p || x -> p e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) <-> ( A. p e. Prime ( p || ( y x. z ) -> p e. S ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) ) )
38 breq2 
 |-  ( x = B -> ( p || x <-> p || B ) )
39 38 imbi1d 
 |-  ( x = B -> ( ( p || x -> p e. S ) <-> ( p || B -> p e. S ) ) )
40 39 ralbidv 
 |-  ( x = B -> ( A. p e. Prime ( p || x -> p e. S ) <-> A. p e. Prime ( p || B -> p e. S ) ) )
41 oveq2 
 |-  ( x = B -> ( m x. x ) = ( m x. B ) )
42 41 eleq1d 
 |-  ( x = B -> ( ( m x. x ) e. S <-> ( m x. B ) e. S ) )
43 42 imbi1d 
 |-  ( x = B -> ( ( ( m x. x ) e. S -> m e. S ) <-> ( ( m x. B ) e. S -> m e. S ) ) )
44 43 ralbidv 
 |-  ( x = B -> ( A. m e. NN ( ( m x. x ) e. S -> m e. S ) <-> A. m e. NN ( ( m x. B ) e. S -> m e. S ) ) )
45 40 44 imbi12d 
 |-  ( x = B -> ( ( A. p e. Prime ( p || x -> p e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) <-> ( A. p e. Prime ( p || B -> p e. S ) -> A. m e. NN ( ( m x. B ) e. S -> m e. S ) ) ) )
46 nncn 
 |-  ( m e. NN -> m e. CC )
47 46 mulridd 
 |-  ( m e. NN -> ( m x. 1 ) = m )
48 47 eleq1d 
 |-  ( m e. NN -> ( ( m x. 1 ) e. S <-> m e. S ) )
49 48 biimpd 
 |-  ( m e. NN -> ( ( m x. 1 ) e. S -> m e. S ) )
50 49 rgen 
 |-  A. m e. NN ( ( m x. 1 ) e. S -> m e. S )
51 50 a1i 
 |-  ( A. p e. Prime ( p || 1 -> p e. S ) -> A. m e. NN ( ( m x. 1 ) e. S -> m e. S ) )
52 breq1 
 |-  ( p = x -> ( p || x <-> x || x ) )
53 eleq1 
 |-  ( p = x -> ( p e. S <-> x e. S ) )
54 52 53 imbi12d 
 |-  ( p = x -> ( ( p || x -> p e. S ) <-> ( x || x -> x e. S ) ) )
55 54 rspcv 
 |-  ( x e. Prime -> ( A. p e. Prime ( p || x -> p e. S ) -> ( x || x -> x e. S ) ) )
56 prmz 
 |-  ( x e. Prime -> x e. ZZ )
57 iddvds 
 |-  ( x e. ZZ -> x || x )
58 56 57 syl 
 |-  ( x e. Prime -> x || x )
59 simprl 
 |-  ( ( ( x e. Prime /\ x e. S ) /\ ( m e. NN /\ ( m x. x ) e. S ) ) -> m e. NN )
60 simpll 
 |-  ( ( ( x e. Prime /\ x e. S ) /\ ( m e. NN /\ ( m x. x ) e. S ) ) -> x e. Prime )
61 simprr 
 |-  ( ( ( x e. Prime /\ x e. S ) /\ ( m e. NN /\ ( m x. x ) e. S ) ) -> ( m x. x ) e. S )
62 simplr 
 |-  ( ( ( x e. Prime /\ x e. S ) /\ ( m e. NN /\ ( m x. x ) e. S ) ) -> x e. S )
63 1 59 60 61 62 2sqlem5 
 |-  ( ( ( x e. Prime /\ x e. S ) /\ ( m e. NN /\ ( m x. x ) e. S ) ) -> m e. S )
64 63 expr 
 |-  ( ( ( x e. Prime /\ x e. S ) /\ m e. NN ) -> ( ( m x. x ) e. S -> m e. S ) )
65 64 ralrimiva 
 |-  ( ( x e. Prime /\ x e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) )
66 65 ex 
 |-  ( x e. Prime -> ( x e. S -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) )
67 58 66 embantd 
 |-  ( x e. Prime -> ( ( x || x -> x e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) )
68 55 67 syld 
 |-  ( x e. Prime -> ( A. p e. Prime ( p || x -> p e. S ) -> A. m e. NN ( ( m x. x ) e. S -> m e. S ) ) )
69 anim12 
 |-  ( ( ( A. p e. Prime ( p || y -> p e. S ) -> A. m e. NN ( ( m x. y ) e. S -> m e. S ) ) /\ ( A. p e. Prime ( p || z -> p e. S ) -> A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) ) -> ( ( A. p e. Prime ( p || y -> p e. S ) /\ A. p e. Prime ( p || z -> p e. S ) ) -> ( A. m e. NN ( ( m x. y ) e. S -> m e. S ) /\ A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) ) )
70 simpr 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> p e. Prime )
71 eluzelz 
 |-  ( y e. ( ZZ>= ` 2 ) -> y e. ZZ )
72 71 ad2antrr 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> y e. ZZ )
73 eluzelz 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. ZZ )
74 73 ad2antlr 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> z e. ZZ )
75 euclemma 
 |-  ( ( p e. Prime /\ y e. ZZ /\ z e. ZZ ) -> ( p || ( y x. z ) <-> ( p || y \/ p || z ) ) )
76 70 72 74 75 syl3anc 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> ( p || ( y x. z ) <-> ( p || y \/ p || z ) ) )
77 76 imbi1d 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> ( ( p || ( y x. z ) -> p e. S ) <-> ( ( p || y \/ p || z ) -> p e. S ) ) )
78 jaob 
 |-  ( ( ( p || y \/ p || z ) -> p e. S ) <-> ( ( p || y -> p e. S ) /\ ( p || z -> p e. S ) ) )
79 77 78 bitrdi 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ p e. Prime ) -> ( ( p || ( y x. z ) -> p e. S ) <-> ( ( p || y -> p e. S ) /\ ( p || z -> p e. S ) ) ) )
80 79 ralbidva 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( A. p e. Prime ( p || ( y x. z ) -> p e. S ) <-> A. p e. Prime ( ( p || y -> p e. S ) /\ ( p || z -> p e. S ) ) ) )
81 r19.26 
 |-  ( A. p e. Prime ( ( p || y -> p e. S ) /\ ( p || z -> p e. S ) ) <-> ( A. p e. Prime ( p || y -> p e. S ) /\ A. p e. Prime ( p || z -> p e. S ) ) )
82 80 81 bitrdi 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( A. p e. Prime ( p || ( y x. z ) -> p e. S ) <-> ( A. p e. Prime ( p || y -> p e. S ) /\ A. p e. Prime ( p || z -> p e. S ) ) ) )
83 82 biimpa 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) -> ( A. p e. Prime ( p || y -> p e. S ) /\ A. p e. Prime ( p || z -> p e. S ) ) )
84 oveq1 
 |-  ( m = n -> ( m x. y ) = ( n x. y ) )
85 84 eleq1d 
 |-  ( m = n -> ( ( m x. y ) e. S <-> ( n x. y ) e. S ) )
86 eleq1 
 |-  ( m = n -> ( m e. S <-> n e. S ) )
87 85 86 imbi12d 
 |-  ( m = n -> ( ( ( m x. y ) e. S -> m e. S ) <-> ( ( n x. y ) e. S -> n e. S ) ) )
88 87 cbvralvw 
 |-  ( A. m e. NN ( ( m x. y ) e. S -> m e. S ) <-> A. n e. NN ( ( n x. y ) e. S -> n e. S ) )
89 46 adantl 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> m e. CC )
90 uzssz 
 |-  ( ZZ>= ` 2 ) C_ ZZ
91 zsscn 
 |-  ZZ C_ CC
92 90 91 sstri 
 |-  ( ZZ>= ` 2 ) C_ CC
93 simpll 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) -> y e. ( ZZ>= ` 2 ) )
94 93 ad2antrr 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> y e. ( ZZ>= ` 2 ) )
95 92 94 sselid 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> y e. CC )
96 simplr 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) -> z e. ( ZZ>= ` 2 ) )
97 96 ad2antrr 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> z e. ( ZZ>= ` 2 ) )
98 92 97 sselid 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> z e. CC )
99 mul32 
 |-  ( ( m e. CC /\ y e. CC /\ z e. CC ) -> ( ( m x. y ) x. z ) = ( ( m x. z ) x. y ) )
100 mulass 
 |-  ( ( m e. CC /\ y e. CC /\ z e. CC ) -> ( ( m x. y ) x. z ) = ( m x. ( y x. z ) ) )
101 99 100 eqtr3d 
 |-  ( ( m e. CC /\ y e. CC /\ z e. CC ) -> ( ( m x. z ) x. y ) = ( m x. ( y x. z ) ) )
102 89 95 98 101 syl3anc 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> ( ( m x. z ) x. y ) = ( m x. ( y x. z ) ) )
103 102 eleq1d 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> ( ( ( m x. z ) x. y ) e. S <-> ( m x. ( y x. z ) ) e. S ) )
104 simpr 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> m e. NN )
105 eluz2nn 
 |-  ( z e. ( ZZ>= ` 2 ) -> z e. NN )
106 97 105 syl 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> z e. NN )
107 104 106 nnmulcld 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> ( m x. z ) e. NN )
108 simplr 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> A. n e. NN ( ( n x. y ) e. S -> n e. S ) )
109 oveq1 
 |-  ( n = ( m x. z ) -> ( n x. y ) = ( ( m x. z ) x. y ) )
110 109 eleq1d 
 |-  ( n = ( m x. z ) -> ( ( n x. y ) e. S <-> ( ( m x. z ) x. y ) e. S ) )
111 eleq1 
 |-  ( n = ( m x. z ) -> ( n e. S <-> ( m x. z ) e. S ) )
112 110 111 imbi12d 
 |-  ( n = ( m x. z ) -> ( ( ( n x. y ) e. S -> n e. S ) <-> ( ( ( m x. z ) x. y ) e. S -> ( m x. z ) e. S ) ) )
113 112 rspcv 
 |-  ( ( m x. z ) e. NN -> ( A. n e. NN ( ( n x. y ) e. S -> n e. S ) -> ( ( ( m x. z ) x. y ) e. S -> ( m x. z ) e. S ) ) )
114 107 108 113 sylc 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> ( ( ( m x. z ) x. y ) e. S -> ( m x. z ) e. S ) )
115 103 114 sylbird 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> ( ( m x. ( y x. z ) ) e. S -> ( m x. z ) e. S ) )
116 115 imim1d 
 |-  ( ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) /\ m e. NN ) -> ( ( ( m x. z ) e. S -> m e. S ) -> ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) )
117 116 ralimdva 
 |-  ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. n e. NN ( ( n x. y ) e. S -> n e. S ) ) -> ( A. m e. NN ( ( m x. z ) e. S -> m e. S ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) )
118 88 117 sylan2b 
 |-  ( ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) /\ A. m e. NN ( ( m x. y ) e. S -> m e. S ) ) -> ( A. m e. NN ( ( m x. z ) e. S -> m e. S ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) )
119 118 expimpd 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) -> ( ( A. m e. NN ( ( m x. y ) e. S -> m e. S ) /\ A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) )
120 83 119 embantd 
 |-  ( ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) /\ A. p e. Prime ( p || ( y x. z ) -> p e. S ) ) -> ( ( ( A. p e. Prime ( p || y -> p e. S ) /\ A. p e. Prime ( p || z -> p e. S ) ) -> ( A. m e. NN ( ( m x. y ) e. S -> m e. S ) /\ A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) )
121 120 ex 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( A. p e. Prime ( p || ( y x. z ) -> p e. S ) -> ( ( ( A. p e. Prime ( p || y -> p e. S ) /\ A. p e. Prime ( p || z -> p e. S ) ) -> ( A. m e. NN ( ( m x. y ) e. S -> m e. S ) /\ A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) ) )
122 121 com23 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( A. p e. Prime ( p || y -> p e. S ) /\ A. p e. Prime ( p || z -> p e. S ) ) -> ( A. m e. NN ( ( m x. y ) e. S -> m e. S ) /\ A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) ) -> ( A. p e. Prime ( p || ( y x. z ) -> p e. S ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) ) )
123 69 122 syl5 
 |-  ( ( y e. ( ZZ>= ` 2 ) /\ z e. ( ZZ>= ` 2 ) ) -> ( ( ( A. p e. Prime ( p || y -> p e. S ) -> A. m e. NN ( ( m x. y ) e. S -> m e. S ) ) /\ ( A. p e. Prime ( p || z -> p e. S ) -> A. m e. NN ( ( m x. z ) e. S -> m e. S ) ) ) -> ( A. p e. Prime ( p || ( y x. z ) -> p e. S ) -> A. m e. NN ( ( m x. ( y x. z ) ) e. S -> m e. S ) ) ) )
124 13 21 29 37 45 51 68 123 prmind 
 |-  ( B e. NN -> ( A. p e. Prime ( p || B -> p e. S ) -> A. m e. NN ( ( m x. B ) e. S -> m e. S ) ) )
125 3 4 124 sylc 
 |-  ( ph -> A. m e. NN ( ( m x. B ) e. S -> m e. S ) )
126 oveq1 
 |-  ( m = A -> ( m x. B ) = ( A x. B ) )
127 126 eleq1d 
 |-  ( m = A -> ( ( m x. B ) e. S <-> ( A x. B ) e. S ) )
128 eleq1 
 |-  ( m = A -> ( m e. S <-> A e. S ) )
129 127 128 imbi12d 
 |-  ( m = A -> ( ( ( m x. B ) e. S -> m e. S ) <-> ( ( A x. B ) e. S -> A e. S ) ) )
130 129 rspcv 
 |-  ( A e. NN -> ( A. m e. NN ( ( m x. B ) e. S -> m e. S ) -> ( ( A x. B ) e. S -> A e. S ) ) )
131 2 125 5 130 syl3c 
 |-  ( ph -> A e. S )