MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgsquad2lem1 Structured version   Visualization version   GIF version

Theorem lgsquad2lem1 26735
Description: Lemma for lgsquad2 26737. (Contributed by Mario Carneiro, 19-Jun-2015.)
Hypotheses
Ref Expression
lgsquad2.1 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
lgsquad2.2 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘€)
lgsquad2.3 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
lgsquad2.4 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘)
lgsquad2.5 (๐œ‘ โ†’ (๐‘€ gcd ๐‘) = 1)
lgsquad2lem1.a (๐œ‘ โ†’ ๐ด โˆˆ โ„•)
lgsquad2lem1.b (๐œ‘ โ†’ ๐ต โˆˆ โ„•)
lgsquad2lem1.m (๐œ‘ โ†’ (๐ด ยท ๐ต) = ๐‘€)
lgsquad2lem1.1 (๐œ‘ โ†’ ((๐ด /L ๐‘) ยท (๐‘ /L ๐ด)) = (-1โ†‘(((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
lgsquad2lem1.2 (๐œ‘ โ†’ ((๐ต /L ๐‘) ยท (๐‘ /L ๐ต)) = (-1โ†‘(((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
Assertion
Ref Expression
lgsquad2lem1 (๐œ‘ โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))

Proof of Theorem lgsquad2lem1
StepHypRef Expression
1 lgsquad2lem1.m . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด ยท ๐ต) = ๐‘€)
2 lgsquad2lem1.a . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ด โˆˆ โ„•)
32nnzd 12527 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ด โˆˆ โ„ค)
43zcnd 12609 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
5 ax-1cn 11110 . . . . . . . . . . . . . 14 1 โˆˆ โ„‚
6 npcan 11411 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐ด โˆ’ 1) + 1) = ๐ด)
74, 5, 6sylancl 587 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ด โˆ’ 1) + 1) = ๐ด)
8 lgsquad2lem1.b . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ต โˆˆ โ„•)
98nnzd 12527 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
109zcnd 12609 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
11 npcan 11411 . . . . . . . . . . . . . 14 ((๐ต โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐ต โˆ’ 1) + 1) = ๐ต)
1210, 5, 11sylancl 587 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ต โˆ’ 1) + 1) = ๐ต)
137, 12oveq12d 7376 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ 1) + 1) ยท ((๐ต โˆ’ 1) + 1)) = (๐ด ยท ๐ต))
14 peano2zm 12547 . . . . . . . . . . . . . . . 16 (๐ด โˆˆ โ„ค โ†’ (๐ด โˆ’ 1) โˆˆ โ„ค)
153, 14syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ด โˆ’ 1) โˆˆ โ„ค)
1615zcnd 12609 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ด โˆ’ 1) โˆˆ โ„‚)
175a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
18 peano2zm 12547 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ โ„ค โ†’ (๐ต โˆ’ 1) โˆˆ โ„ค)
199, 18syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ต โˆ’ 1) โˆˆ โ„ค)
2019zcnd 12609 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ต โˆ’ 1) โˆˆ โ„‚)
2116, 17, 20, 17muladdd 11614 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐ด โˆ’ 1) + 1) ยท ((๐ต โˆ’ 1) + 1)) = ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + (1 ยท 1)) + (((๐ด โˆ’ 1) ยท 1) + ((๐ต โˆ’ 1) ยท 1))))
22 1t1e1 12316 . . . . . . . . . . . . . . . 16 (1 ยท 1) = 1
2322a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (1 ยท 1) = 1)
2423oveq2d 7374 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + (1 ยท 1)) = (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1))
2516mulid1d 11173 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ด โˆ’ 1) ยท 1) = (๐ด โˆ’ 1))
2620mulid1d 11173 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต โˆ’ 1) ยท 1) = (๐ต โˆ’ 1))
2725, 26oveq12d 7376 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ด โˆ’ 1) ยท 1) + ((๐ต โˆ’ 1) ยท 1)) = ((๐ด โˆ’ 1) + (๐ต โˆ’ 1)))
2824, 27oveq12d 7376 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + (1 ยท 1)) + (((๐ด โˆ’ 1) ยท 1) + ((๐ต โˆ’ 1) ยท 1))) = ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))))
2921, 28eqtrd 2777 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ 1) + 1) ยท ((๐ต โˆ’ 1) + 1)) = ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))))
3013, 29eqtr3d 2779 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด ยท ๐ต) = ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))))
311, 30eqtr3d 2779 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ = ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))))
3231oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘€ โˆ’ 1) = (((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))) โˆ’ 1))
3316, 20mulcld 11176 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) โˆˆ โ„‚)
34 addcl 11134 . . . . . . . . . . 11 ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) โˆˆ โ„‚)
3533, 5, 34sylancl 587 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) โˆˆ โ„‚)
3616, 20addcld 11175 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด โˆ’ 1) + (๐ต โˆ’ 1)) โˆˆ โ„‚)
3735, 36, 17addsubd 11534 . . . . . . . . 9 (๐œ‘ โ†’ (((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))) โˆ’ 1) = (((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) โˆ’ 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))))
38 pncan 11408 . . . . . . . . . . 11 ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) โˆ’ 1) = ((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)))
3933, 5, 38sylancl 587 . . . . . . . . . 10 (๐œ‘ โ†’ ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) โˆ’ 1) = ((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)))
4039oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ (((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + 1) โˆ’ 1) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))) = (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))))
4132, 37, 403eqtrd 2781 . . . . . . . 8 (๐œ‘ โ†’ (๐‘€ โˆ’ 1) = (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))))
4241oveq1d 7373 . . . . . . 7 (๐œ‘ โ†’ ((๐‘€ โˆ’ 1) / 2) = ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))) / 2))
43 2cnd 12232 . . . . . . . 8 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
44 2ne0 12258 . . . . . . . . 9 2 โ‰  0
4544a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2 โ‰  0)
4633, 36, 43, 45divdird 11970 . . . . . . 7 (๐œ‘ โ†’ ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) + ((๐ด โˆ’ 1) + (๐ต โˆ’ 1))) / 2) = ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) / 2) + (((๐ด โˆ’ 1) + (๐ต โˆ’ 1)) / 2)))
4716, 20, 43, 45divassd 11967 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) / 2) = ((๐ด โˆ’ 1) ยท ((๐ต โˆ’ 1) / 2)))
4816, 43, 45divcan2d 11934 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท ((๐ด โˆ’ 1) / 2)) = (๐ด โˆ’ 1))
4948oveq1d 7373 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ((๐ด โˆ’ 1) / 2)) ยท ((๐ต โˆ’ 1) / 2)) = ((๐ด โˆ’ 1) ยท ((๐ต โˆ’ 1) / 2)))
50 lgsquad2.2 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘€)
51 dvdsmul1 16161 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ๐ด โˆฅ (๐ด ยท ๐ต))
523, 9, 51syl2anc 585 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ด โˆฅ (๐ด ยท ๐ต))
5352, 1breqtrd 5132 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ด โˆฅ ๐‘€)
54 2z 12536 . . . . . . . . . . . . . . . 16 2 โˆˆ โ„ค
55 lgsquad2.1 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
5655nnzd 12527 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
57 dvdstr 16177 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„ค โˆง ๐ด โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((2 โˆฅ ๐ด โˆง ๐ด โˆฅ ๐‘€) โ†’ 2 โˆฅ ๐‘€))
5854, 3, 56, 57mp3an2i 1467 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 โˆฅ ๐ด โˆง ๐ด โˆฅ ๐‘€) โ†’ 2 โˆฅ ๐‘€))
5953, 58mpan2d 693 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 โˆฅ ๐ด โ†’ 2 โˆฅ ๐‘€))
6050, 59mtod 197 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐ด)
61 1zzd 12535 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
62 2prm 16569 . . . . . . . . . . . . . 14 2 โˆˆ โ„™
63 nprmdvds1 16583 . . . . . . . . . . . . . 14 (2 โˆˆ โ„™ โ†’ ยฌ 2 โˆฅ 1)
6462, 63mp1i 13 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ยฌ 2 โˆฅ 1)
65 omoe 16247 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐ด) โˆง (1 โˆˆ โ„ค โˆง ยฌ 2 โˆฅ 1)) โ†’ 2 โˆฅ (๐ด โˆ’ 1))
663, 60, 61, 64, 65syl22anc 838 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆฅ (๐ด โˆ’ 1))
67 dvdsval2 16140 . . . . . . . . . . . . 13 ((2 โˆˆ โ„ค โˆง 2 โ‰  0 โˆง (๐ด โˆ’ 1) โˆˆ โ„ค) โ†’ (2 โˆฅ (๐ด โˆ’ 1) โ†” ((๐ด โˆ’ 1) / 2) โˆˆ โ„ค))
6854, 45, 15, 67mp3an2i 1467 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 โˆฅ (๐ด โˆ’ 1) โ†” ((๐ด โˆ’ 1) / 2) โˆˆ โ„ค))
6966, 68mpbid 231 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ด โˆ’ 1) / 2) โˆˆ โ„ค)
7069zcnd 12609 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด โˆ’ 1) / 2) โˆˆ โ„‚)
71 dvdsmul2 16162 . . . . . . . . . . . . . . . . 17 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ ๐ต โˆฅ (๐ด ยท ๐ต))
723, 9, 71syl2anc 585 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ต โˆฅ (๐ด ยท ๐ต))
7372, 1breqtrd 5132 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ต โˆฅ ๐‘€)
74 dvdstr 16177 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค) โ†’ ((2 โˆฅ ๐ต โˆง ๐ต โˆฅ ๐‘€) โ†’ 2 โˆฅ ๐‘€))
7554, 9, 56, 74mp3an2i 1467 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 โˆฅ ๐ต โˆง ๐ต โˆฅ ๐‘€) โ†’ 2 โˆฅ ๐‘€))
7673, 75mpan2d 693 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 โˆฅ ๐ต โ†’ 2 โˆฅ ๐‘€))
7750, 76mtod 197 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐ต)
78 omoe 16247 . . . . . . . . . . . . 13 (((๐ต โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐ต) โˆง (1 โˆˆ โ„ค โˆง ยฌ 2 โˆฅ 1)) โ†’ 2 โˆฅ (๐ต โˆ’ 1))
799, 77, 61, 64, 78syl22anc 838 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆฅ (๐ต โˆ’ 1))
80 dvdsval2 16140 . . . . . . . . . . . . 13 ((2 โˆˆ โ„ค โˆง 2 โ‰  0 โˆง (๐ต โˆ’ 1) โˆˆ โ„ค) โ†’ (2 โˆฅ (๐ต โˆ’ 1) โ†” ((๐ต โˆ’ 1) / 2) โˆˆ โ„ค))
8154, 45, 19, 80mp3an2i 1467 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 โˆฅ (๐ต โˆ’ 1) โ†” ((๐ต โˆ’ 1) / 2) โˆˆ โ„ค))
8279, 81mpbid 231 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ต โˆ’ 1) / 2) โˆˆ โ„ค)
8382zcnd 12609 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต โˆ’ 1) / 2) โˆˆ โ„‚)
8443, 70, 83mulassd 11179 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ((๐ด โˆ’ 1) / 2)) ยท ((๐ต โˆ’ 1) / 2)) = (2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))))
8547, 49, 843eqtr2d 2783 . . . . . . . 8 (๐œ‘ โ†’ (((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) / 2) = (2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))))
8616, 20, 43, 45divdird 11970 . . . . . . . 8 (๐œ‘ โ†’ (((๐ด โˆ’ 1) + (๐ต โˆ’ 1)) / 2) = (((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)))
8785, 86oveq12d 7376 . . . . . . 7 (๐œ‘ โ†’ ((((๐ด โˆ’ 1) ยท (๐ต โˆ’ 1)) / 2) + (((๐ด โˆ’ 1) + (๐ต โˆ’ 1)) / 2)) = ((2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) + (((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2))))
8842, 46, 873eqtrd 2781 . . . . . 6 (๐œ‘ โ†’ ((๐‘€ โˆ’ 1) / 2) = ((2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) + (((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2))))
8988oveq1d 7373 . . . . 5 (๐œ‘ โ†’ (((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (((2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) + (((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2))) ยท ((๐‘ โˆ’ 1) / 2)))
9054a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 2 โˆˆ โ„ค)
9169, 82zmulcld 12614 . . . . . . . 8 (๐œ‘ โ†’ (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) โˆˆ โ„ค)
9290, 91zmulcld 12614 . . . . . . 7 (๐œ‘ โ†’ (2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) โˆˆ โ„ค)
9392zcnd 12609 . . . . . 6 (๐œ‘ โ†’ (2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) โˆˆ โ„‚)
9469, 82zaddcld 12612 . . . . . . 7 (๐œ‘ โ†’ (((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) โˆˆ โ„ค)
9594zcnd 12609 . . . . . 6 (๐œ‘ โ†’ (((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) โˆˆ โ„‚)
96 lgsquad2.3 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
9796nnzd 12527 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
98 lgsquad2.4 . . . . . . . . 9 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘)
99 omoe 16247 . . . . . . . . 9 (((๐‘ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘) โˆง (1 โˆˆ โ„ค โˆง ยฌ 2 โˆฅ 1)) โ†’ 2 โˆฅ (๐‘ โˆ’ 1))
10097, 98, 61, 64, 99syl22anc 838 . . . . . . . 8 (๐œ‘ โ†’ 2 โˆฅ (๐‘ โˆ’ 1))
101 peano2zm 12547 . . . . . . . . . 10 (๐‘ โˆˆ โ„ค โ†’ (๐‘ โˆ’ 1) โˆˆ โ„ค)
10297, 101syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ โˆ’ 1) โˆˆ โ„ค)
103 dvdsval2 16140 . . . . . . . . 9 ((2 โˆˆ โ„ค โˆง 2 โ‰  0 โˆง (๐‘ โˆ’ 1) โˆˆ โ„ค) โ†’ (2 โˆฅ (๐‘ โˆ’ 1) โ†” ((๐‘ โˆ’ 1) / 2) โˆˆ โ„ค))
10454, 45, 102, 103mp3an2i 1467 . . . . . . . 8 (๐œ‘ โ†’ (2 โˆฅ (๐‘ โˆ’ 1) โ†” ((๐‘ โˆ’ 1) / 2) โˆˆ โ„ค))
105100, 104mpbid 231 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ โˆ’ 1) / 2) โˆˆ โ„ค)
106105zcnd 12609 . . . . . 6 (๐œ‘ โ†’ ((๐‘ โˆ’ 1) / 2) โˆˆ โ„‚)
10793, 95, 106adddird 11181 . . . . 5 (๐œ‘ โ†’ (((2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) + (((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2))) ยท ((๐‘ โˆ’ 1) / 2)) = (((2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) ยท ((๐‘ โˆ’ 1) / 2)) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))))
10891zcnd 12609 . . . . . . 7 (๐œ‘ โ†’ (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) โˆˆ โ„‚)
10943, 108, 106mulassd 11179 . . . . . 6 (๐œ‘ โ†’ ((2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) ยท ((๐‘ โˆ’ 1) / 2)) = (2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))))
110109oveq1d 7373 . . . . 5 (๐œ‘ โ†’ (((2 ยท (((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2))) ยท ((๐‘ โˆ’ 1) / 2)) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) = ((2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))))
11189, 107, 1103eqtrd 2781 . . . 4 (๐œ‘ โ†’ (((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = ((2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))))
112111oveq2d 7374 . . 3 (๐œ‘ โ†’ (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘((2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))))
113 neg1cn 12268 . . . . . 6 -1 โˆˆ โ„‚
114113a1i 11 . . . . 5 (๐œ‘ โ†’ -1 โˆˆ โ„‚)
115 neg1ne0 12270 . . . . . 6 -1 โ‰  0
116115a1i 11 . . . . 5 (๐œ‘ โ†’ -1 โ‰  0)
11791, 105zmulcld 12614 . . . . . 6 (๐œ‘ โ†’ ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค)
11890, 117zmulcld 12614 . . . . 5 (๐œ‘ โ†’ (2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) โˆˆ โ„ค)
11994, 105zmulcld 12614 . . . . 5 (๐œ‘ โ†’ ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค)
120 expaddz 14013 . . . . 5 (((-1 โˆˆ โ„‚ โˆง -1 โ‰  0) โˆง ((2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) โˆˆ โ„ค โˆง ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค)) โ†’ (-1โ†‘((2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = ((-1โ†‘(2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) ยท (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))))
121114, 116, 118, 119, 120syl22anc 838 . . . 4 (๐œ‘ โ†’ (-1โ†‘((2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = ((-1โ†‘(2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) ยท (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))))
122 expmulz 14015 . . . . . . 7 (((-1 โˆˆ โ„‚ โˆง -1 โ‰  0) โˆง (2 โˆˆ โ„ค โˆง ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค)) โ†’ (-1โ†‘(2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = ((-1โ†‘2)โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))))
123114, 116, 90, 117, 122syl22anc 838 . . . . . 6 (๐œ‘ โ†’ (-1โ†‘(2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = ((-1โ†‘2)โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))))
124 neg1sqe1 14101 . . . . . . . 8 (-1โ†‘2) = 1
125124oveq1i 7368 . . . . . . 7 ((-1โ†‘2)โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) = (1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))
126 1exp 13998 . . . . . . . 8 (((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค โ†’ (1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) = 1)
127117, 126syl 17 . . . . . . 7 (๐œ‘ โ†’ (1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) = 1)
128125, 127eqtrid 2789 . . . . . 6 (๐œ‘ โ†’ ((-1โ†‘2)โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) = 1)
129123, 128eqtrd 2777 . . . . 5 (๐œ‘ โ†’ (-1โ†‘(2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = 1)
130129oveq1d 7373 . . . 4 (๐œ‘ โ†’ ((-1โ†‘(2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) ยท (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = (1 ยท (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))))
131121, 130eqtrd 2777 . . 3 (๐œ‘ โ†’ (-1โ†‘((2 ยท ((((๐ด โˆ’ 1) / 2) ยท ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) + ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = (1 ยท (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))))
132114, 116, 119expclzd 14057 . . . . 5 (๐œ‘ โ†’ (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) โˆˆ โ„‚)
133132mulid2d 11174 . . . 4 (๐œ‘ โ†’ (1 ยท (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))))
13470, 83, 106adddird 11181 . . . . 5 (๐œ‘ โ†’ ((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)) = ((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) + (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
135134oveq2d 7374 . . . 4 (๐œ‘ โ†’ (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) + (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
136133, 135eqtrd 2777 . . 3 (๐œ‘ โ†’ (1 ยท (-1โ†‘((((๐ด โˆ’ 1) / 2) + ((๐ต โˆ’ 1) / 2)) ยท ((๐‘ โˆ’ 1) / 2)))) = (-1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) + (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
137112, 131, 1363eqtrd 2781 . 2 (๐œ‘ โ†’ (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) + (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
138 lgsquad2lem1.1 . . . 4 (๐œ‘ โ†’ ((๐ด /L ๐‘) ยท (๐‘ /L ๐ด)) = (-1โ†‘(((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
139 lgsquad2lem1.2 . . . 4 (๐œ‘ โ†’ ((๐ต /L ๐‘) ยท (๐‘ /L ๐ต)) = (-1โ†‘(((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
140138, 139oveq12d 7376 . . 3 (๐œ‘ โ†’ (((๐ด /L ๐‘) ยท (๐‘ /L ๐ด)) ยท ((๐ต /L ๐‘) ยท (๐‘ /L ๐ต))) = ((-1โ†‘(((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) ยท (-1โ†‘(((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
14169, 105zmulcld 12614 . . . 4 (๐œ‘ โ†’ (((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค)
14282, 105zmulcld 12614 . . . 4 (๐œ‘ โ†’ (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค)
143 expaddz 14013 . . . 4 (((-1 โˆˆ โ„‚ โˆง -1 โ‰  0) โˆง ((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค โˆง (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) โˆˆ โ„ค)) โ†’ (-1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) + (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) = ((-1โ†‘(((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) ยท (-1โ†‘(((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
144114, 116, 141, 142, 143syl22anc 838 . . 3 (๐œ‘ โ†’ (-1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) + (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) = ((-1โ†‘(((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) ยท (-1โ†‘(((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
145140, 144eqtr4d 2780 . 2 (๐œ‘ โ†’ (((๐ด /L ๐‘) ยท (๐‘ /L ๐ด)) ยท ((๐ต /L ๐‘) ยท (๐‘ /L ๐ต))) = (-1โ†‘((((๐ด โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) + (((๐ต โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
146 lgscl 26662 . . . . . 6 ((๐ด โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐ด /L ๐‘) โˆˆ โ„ค)
1473, 97, 146syl2anc 585 . . . . 5 (๐œ‘ โ†’ (๐ด /L ๐‘) โˆˆ โ„ค)
148147zcnd 12609 . . . 4 (๐œ‘ โ†’ (๐ด /L ๐‘) โˆˆ โ„‚)
149 lgscl 26662 . . . . . 6 ((๐ต โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (๐ต /L ๐‘) โˆˆ โ„ค)
1509, 97, 149syl2anc 585 . . . . 5 (๐œ‘ โ†’ (๐ต /L ๐‘) โˆˆ โ„ค)
151150zcnd 12609 . . . 4 (๐œ‘ โ†’ (๐ต /L ๐‘) โˆˆ โ„‚)
152 lgscl 26662 . . . . . 6 ((๐‘ โˆˆ โ„ค โˆง ๐ด โˆˆ โ„ค) โ†’ (๐‘ /L ๐ด) โˆˆ โ„ค)
15397, 3, 152syl2anc 585 . . . . 5 (๐œ‘ โ†’ (๐‘ /L ๐ด) โˆˆ โ„ค)
154153zcnd 12609 . . . 4 (๐œ‘ โ†’ (๐‘ /L ๐ด) โˆˆ โ„‚)
155 lgscl 26662 . . . . . 6 ((๐‘ โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐‘ /L ๐ต) โˆˆ โ„ค)
15697, 9, 155syl2anc 585 . . . . 5 (๐œ‘ โ†’ (๐‘ /L ๐ต) โˆˆ โ„ค)
157156zcnd 12609 . . . 4 (๐œ‘ โ†’ (๐‘ /L ๐ต) โˆˆ โ„‚)
158148, 151, 154, 157mul4d 11368 . . 3 (๐œ‘ โ†’ (((๐ด /L ๐‘) ยท (๐ต /L ๐‘)) ยท ((๐‘ /L ๐ด) ยท (๐‘ /L ๐ต))) = (((๐ด /L ๐‘) ยท (๐‘ /L ๐ด)) ยท ((๐ต /L ๐‘) ยท (๐‘ /L ๐ต))))
1592nnne0d 12204 . . . . . 6 (๐œ‘ โ†’ ๐ด โ‰  0)
1608nnne0d 12204 . . . . . 6 (๐œ‘ โ†’ ๐ต โ‰  0)
161 lgsdir 26683 . . . . . 6 (((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โˆง (๐ด โ‰  0 โˆง ๐ต โ‰  0)) โ†’ ((๐ด ยท ๐ต) /L ๐‘) = ((๐ด /L ๐‘) ยท (๐ต /L ๐‘)))
1623, 9, 97, 159, 160, 161syl32anc 1379 . . . . 5 (๐œ‘ โ†’ ((๐ด ยท ๐ต) /L ๐‘) = ((๐ด /L ๐‘) ยท (๐ต /L ๐‘)))
1631oveq1d 7373 . . . . 5 (๐œ‘ โ†’ ((๐ด ยท ๐ต) /L ๐‘) = (๐‘€ /L ๐‘))
164162, 163eqtr3d 2779 . . . 4 (๐œ‘ โ†’ ((๐ด /L ๐‘) ยท (๐ต /L ๐‘)) = (๐‘€ /L ๐‘))
165 lgsdi 26685 . . . . . 6 (((๐‘ โˆˆ โ„ค โˆง ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โˆง (๐ด โ‰  0 โˆง ๐ต โ‰  0)) โ†’ (๐‘ /L (๐ด ยท ๐ต)) = ((๐‘ /L ๐ด) ยท (๐‘ /L ๐ต)))
16697, 3, 9, 159, 160, 165syl32anc 1379 . . . . 5 (๐œ‘ โ†’ (๐‘ /L (๐ด ยท ๐ต)) = ((๐‘ /L ๐ด) ยท (๐‘ /L ๐ต)))
1671oveq2d 7374 . . . . 5 (๐œ‘ โ†’ (๐‘ /L (๐ด ยท ๐ต)) = (๐‘ /L ๐‘€))
168166, 167eqtr3d 2779 . . . 4 (๐œ‘ โ†’ ((๐‘ /L ๐ด) ยท (๐‘ /L ๐ต)) = (๐‘ /L ๐‘€))
169164, 168oveq12d 7376 . . 3 (๐œ‘ โ†’ (((๐ด /L ๐‘) ยท (๐ต /L ๐‘)) ยท ((๐‘ /L ๐ด) ยท (๐‘ /L ๐ต))) = ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)))
170158, 169eqtr3d 2779 . 2 (๐œ‘ โ†’ (((๐ด /L ๐‘) ยท (๐‘ /L ๐ด)) ยท ((๐ต /L ๐‘) ยท (๐‘ /L ๐ต))) = ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)))
171137, 145, 1703eqtr2rd 2784 1 (๐œ‘ โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944   class class class wbr 5106  (class class class)co 7358  โ„‚cc 11050  0cc0 11052  1c1 11053   + caddc 11055   ยท cmul 11057   โˆ’ cmin 11386  -cneg 11387   / cdiv 11813  โ„•cn 12154  2c2 12209  โ„คcz 12500  โ†‘cexp 13968   โˆฅ cdvds 16137   gcd cgcd 16375  โ„™cprime 16548   /L clgs 26645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-sup 9379  df-inf 9380  df-dju 9838  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-n0 12415  df-xnn0 12487  df-z 12501  df-uz 12765  df-q 12875  df-rp 12917  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-dvds 16138  df-gcd 16376  df-prm 16549  df-phi 16639  df-pc 16710  df-lgs 26646
This theorem is referenced by:  lgsquad2lem2  26736
  Copyright terms: Public domain W3C validator