Metamath Proof Explorer


Theorem lcmfunsnlem2

Description: Lemma for lcmfunsn and lcmfunsnlem (Induction step part 2). (Contributed by AV, 26-Aug-2020)

Ref Expression
Assertion lcmfunsnlem2 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n n lcm _ y z n = lcm _ y z lcm n

Proof

Step Hyp Ref Expression
1 nfv n z y y Fin
2 nfv n k m y m k lcm _ y k
3 nfra1 n n lcm _ y n = lcm _ y lcm n
4 2 3 nfan n k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n
5 1 4 nfan n z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n
6 0z 0
7 eqoreldif 0 n n = 0 n 0
8 6 7 ax-mp n n = 0 n 0
9 simp2 z y y Fin y
10 snssi z z
11 10 3ad2ant1 z y y Fin z
12 9 11 unssd z y y Fin y z
13 snssi 0 0
14 6 13 mp1i z y y Fin 0
15 12 14 unssd z y y Fin y z 0
16 c0ex 0 V
17 16 snid 0 0
18 17 olci 0 y z 0 0
19 elun 0 y z 0 0 y z 0 0
20 18 19 mpbir 0 y z 0
21 lcmf0val y z 0 0 y z 0 lcm _ y z 0 = 0
22 15 20 21 sylancl z y y Fin lcm _ y z 0 = 0
23 22 adantr z y y Fin n = 0 lcm _ y z 0 = 0
24 sneq n = 0 n = 0
25 24 adantl z y y Fin n = 0 n = 0
26 25 uneq2d z y y Fin n = 0 y z n = y z 0
27 26 fveq2d z y y Fin n = 0 lcm _ y z n = lcm _ y z 0
28 oveq2 n = 0 lcm _ y z lcm n = lcm _ y z lcm 0
29 snfi z Fin
30 unfi y Fin z Fin y z Fin
31 29 30 mpan2 y Fin y z Fin
32 31 3ad2ant3 z y y Fin y z Fin
33 lcmfcl y z y z Fin lcm _ y z 0
34 12 32 33 syl2anc z y y Fin lcm _ y z 0
35 34 nn0zd z y y Fin lcm _ y z
36 lcm0val lcm _ y z lcm _ y z lcm 0 = 0
37 35 36 syl z y y Fin lcm _ y z lcm 0 = 0
38 28 37 sylan9eqr z y y Fin n = 0 lcm _ y z lcm n = 0
39 23 27 38 3eqtr4d z y y Fin n = 0 lcm _ y z n = lcm _ y z lcm n
40 39 ex z y y Fin n = 0 lcm _ y z n = lcm _ y z lcm n
41 40 adantr z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n n = 0 lcm _ y z n = lcm _ y z lcm n
42 41 com12 n = 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
43 9 adantl 0 y n 0 z y y Fin y
44 11 adantl 0 y n 0 z y y Fin z
45 43 44 unssd 0 y n 0 z y y Fin y z
46 elun1 0 y 0 y z
47 46 ad2antrr 0 y n 0 z y y Fin 0 y z
48 lcmf0val y z 0 y z lcm _ y z = 0
49 45 47 48 syl2anc 0 y n 0 z y y Fin lcm _ y z = 0
50 49 oveq2d 0 y n 0 z y y Fin n lcm lcm _ y z = n lcm 0
51 eldifi n 0 n
52 lcm0val n n lcm 0 = 0
53 51 52 syl n 0 n lcm 0 = 0
54 53 ad2antlr 0 y n 0 z y y Fin n lcm 0 = 0
55 50 54 eqtrd 0 y n 0 z y y Fin n lcm lcm _ y z = 0
56 simp3 z y y Fin y Fin
57 56 29 30 sylancl z y y Fin y z Fin
58 12 57 33 syl2anc z y y Fin lcm _ y z 0
59 58 nn0zd z y y Fin lcm _ y z
60 51 adantl 0 y n 0 n
61 lcmcom lcm _ y z n lcm _ y z lcm n = n lcm lcm _ y z
62 59 60 61 syl2anr 0 y n 0 z y y Fin lcm _ y z lcm n = n lcm lcm _ y z
63 12 adantl 0 y n 0 z y y Fin y z
64 51 snssd n 0 n
65 64 ad2antlr 0 y n 0 z y y Fin n
66 63 65 unssd 0 y n 0 z y y Fin y z n
67 46 orcd 0 y 0 y z 0 n
68 elun 0 y z n 0 y z 0 n
69 67 68 sylibr 0 y 0 y z n
70 69 ad2antrr 0 y n 0 z y y Fin 0 y z n
71 lcmf0val y z n 0 y z n lcm _ y z n = 0
72 66 70 71 syl2anc 0 y n 0 z y y Fin lcm _ y z n = 0
73 55 62 72 3eqtr4rd 0 y n 0 z y y Fin lcm _ y z n = lcm _ y z lcm n
74 73 a1d 0 y n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
75 74 expimpd 0 y n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
76 75 ex 0 y n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
77 elsng 0 0 z 0 = z
78 eqcom 0 = z z = 0
79 77 78 bitrdi 0 0 z z = 0
80 6 79 ax-mp 0 z z = 0
81 80 biimpri z = 0 0 z
82 81 ad2antrr z = 0 n 0 z y y Fin 0 z
83 82 olcd z = 0 n 0 z y y Fin 0 y 0 z
84 elun 0 y z 0 y 0 z
85 83 84 sylibr z = 0 n 0 z y y Fin 0 y z
86 12 85 48 syl2an2 z = 0 n 0 z y y Fin lcm _ y z = 0
87 86 oveq2d z = 0 n 0 z y y Fin n lcm lcm _ y z = n lcm 0
88 51 ad2antlr z = 0 n 0 z y y Fin n
89 88 52 syl z = 0 n 0 z y y Fin n lcm 0 = 0
90 87 89 eqtrd z = 0 n 0 z y y Fin n lcm lcm _ y z = 0
91 59 88 61 syl2an2 z = 0 n 0 z y y Fin lcm _ y z lcm n = n lcm lcm _ y z
92 12 adantl z = 0 n 0 z y y Fin y z
93 64 ad2antlr z = 0 n 0 z y y Fin n
94 92 93 unssd z = 0 n 0 z y y Fin y z n
95 sneq z = 0 z = 0
96 17 95 eleqtrrid z = 0 0 z
97 96 ad2antrr z = 0 n 0 z y y Fin 0 z
98 97 olcd z = 0 n 0 z y y Fin 0 y 0 z
99 98 84 sylibr z = 0 n 0 z y y Fin 0 y z
100 99 orcd z = 0 n 0 z y y Fin 0 y z 0 n
101 100 68 sylibr z = 0 n 0 z y y Fin 0 y z n
102 94 101 71 syl2anc z = 0 n 0 z y y Fin lcm _ y z n = 0
103 90 91 102 3eqtr4rd z = 0 n 0 z y y Fin lcm _ y z n = lcm _ y z lcm n
104 103 a1d z = 0 n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
105 104 expimpd z = 0 n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
106 105 ex z = 0 n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
107 ioran ¬ 0 y z = 0 ¬ 0 y ¬ z = 0
108 df-nel 0 y ¬ 0 y
109 df-ne z 0 ¬ z = 0
110 108 109 anbi12i 0 y z 0 ¬ 0 y ¬ z = 0
111 107 110 bitr4i ¬ 0 y z = 0 0 y z 0
112 eldif n 0 n ¬ n 0
113 velsn n 0 n = 0
114 113 bicomi n = 0 n 0
115 114 necon3abii n 0 ¬ n 0
116 lcmfunsnlem2lem2 0 y z 0 n 0 n z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
117 116 exp520 0 y z 0 n 0 n z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
118 117 imp 0 y z 0 n 0 n z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
119 115 118 syl5bir 0 y z 0 ¬ n 0 n z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
120 119 impcomd 0 y z 0 n ¬ n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
121 112 120 syl5bi 0 y z 0 n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
122 111 121 sylbi ¬ 0 y z = 0 n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
123 76 106 122 ecase3 n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
124 42 123 jaoi n = 0 n 0 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
125 8 124 sylbi n z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n lcm _ y z n = lcm _ y z lcm n
126 125 com12 z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n n lcm _ y z n = lcm _ y z lcm n
127 5 126 ralrimi z y y Fin k m y m k lcm _ y k n lcm _ y n = lcm _ y lcm n n lcm _ y z n = lcm _ y z lcm n