Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tgoldbach Structured version   Visualization version   GIF version

Theorem tgoldbach 46471
Description: The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 46470 and ax-tgoldbachgt 46465. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.)
Assertion
Ref Expression
tgoldbach โˆ€๐‘› โˆˆ Odd (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )

Proof of Theorem tgoldbach
Dummy variables ๐‘š ๐‘œ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oddz 46285 . . . . 5 (๐‘› โˆˆ Odd โ†’ ๐‘› โˆˆ โ„ค)
21zred 12662 . . . 4 (๐‘› โˆˆ Odd โ†’ ๐‘› โˆˆ โ„)
3 10re 12692 . . . . 5 10 โˆˆ โ„
4 2nn0 12485 . . . . . . 7 2 โˆˆ โ„•0
5 7nn 12300 . . . . . . 7 7 โˆˆ โ„•
64, 5decnncl 12693 . . . . . 6 27 โˆˆ โ„•
76nnnn0i 12476 . . . . 5 27 โˆˆ โ„•0
8 reexpcl 14040 . . . . 5 ((10 โˆˆ โ„ โˆง 27 โˆˆ โ„•0) โ†’ (10โ†‘27) โˆˆ โ„)
93, 7, 8mp2an 690 . . . 4 (10โ†‘27) โˆˆ โ„
10 lelttric 11317 . . . 4 ((๐‘› โˆˆ โ„ โˆง (10โ†‘27) โˆˆ โ„) โ†’ (๐‘› โ‰ค (10โ†‘27) โˆจ (10โ†‘27) < ๐‘›))
112, 9, 10sylancl 586 . . 3 (๐‘› โˆˆ Odd โ†’ (๐‘› โ‰ค (10โ†‘27) โˆจ (10โ†‘27) < ๐‘›))
12 tgoldbachlt 46470 . . . . 5 โˆƒ๐‘š โˆˆ โ„• ((8 ยท (10โ†‘30)) < ๐‘š โˆง โˆ€๐‘œ โˆˆ Odd ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd ))
13 breq2 5151 . . . . . . . . . . . . 13 (๐‘œ = ๐‘› โ†’ (7 < ๐‘œ โ†” 7 < ๐‘›))
14 breq1 5150 . . . . . . . . . . . . 13 (๐‘œ = ๐‘› โ†’ (๐‘œ < ๐‘š โ†” ๐‘› < ๐‘š))
1513, 14anbi12d 631 . . . . . . . . . . . 12 (๐‘œ = ๐‘› โ†’ ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†” (7 < ๐‘› โˆง ๐‘› < ๐‘š)))
16 eleq1w 2816 . . . . . . . . . . . 12 (๐‘œ = ๐‘› โ†’ (๐‘œ โˆˆ GoldbachOdd โ†” ๐‘› โˆˆ GoldbachOdd ))
1715, 16imbi12d 344 . . . . . . . . . . 11 (๐‘œ = ๐‘› โ†’ (((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†” ((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd )))
1817rspcv 3608 . . . . . . . . . 10 (๐‘› โˆˆ Odd โ†’ (โˆ€๐‘œ โˆˆ Odd ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†’ ((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd )))
199recni 11224 . . . . . . . . . . . . . . . . . . . . . . 23 (10โ†‘27) โˆˆ โ„‚
2019mullidi 11215 . . . . . . . . . . . . . . . . . . . . . 22 (1 ยท (10โ†‘27)) = (10โ†‘27)
21 1re 11210 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 โˆˆ โ„
22 8re 12304 . . . . . . . . . . . . . . . . . . . . . . . . 25 8 โˆˆ โ„
2321, 22pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 โˆˆ โ„ โˆง 8 โˆˆ โ„)
2423a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (1 โˆˆ โ„ โˆง 8 โˆˆ โ„))
25 0le1 11733 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 โ‰ค 1
26 1lt8 12406 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 < 8
2725, 26pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 โ‰ค 1 โˆง 1 < 8)
2827a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (0 โ‰ค 1 โˆง 1 < 8))
29 3nn 12287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 โˆˆ โ„•
3029decnncl2 12697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 30 โˆˆ โ„•
3130nnnn0i 12476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 30 โˆˆ โ„•0
32 reexpcl 14040 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((10 โˆˆ โ„ โˆง 30 โˆˆ โ„•0) โ†’ (10โ†‘30) โˆˆ โ„)
333, 31, 32mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (10โ†‘30) โˆˆ โ„
349, 33pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . 24 ((10โ†‘27) โˆˆ โ„ โˆง (10โ†‘30) โˆˆ โ„)
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ ((10โ†‘27) โˆˆ โ„ โˆง (10โ†‘30) โˆˆ โ„))
36 10nn0 12691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 10 โˆˆ โ„•0
3736, 7nn0expcli 14050 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (10โ†‘27) โˆˆ โ„•0
3837nn0ge0i 12495 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 โ‰ค (10โ†‘27)
396nnzi 12582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 27 โˆˆ โ„ค
4030nnzi 12582 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 30 โˆˆ โ„ค
413, 39, 403pm3.2i 1339 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (10 โˆˆ โ„ โˆง 27 โˆˆ โ„ค โˆง 30 โˆˆ โ„ค)
42 1lt10 12812 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 < 10
43 3nn0 12486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 โˆˆ โ„•0
44 7nn0 12490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 7 โˆˆ โ„•0
45 0nn0 12483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 โˆˆ โ„•0
46 7lt10 12806 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 7 < 10
47 2lt3 12380 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 < 3
484, 43, 44, 45, 46, 47decltc 12702 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 27 < 30
4942, 48pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 < 10 โˆง 27 < 30)
50 ltexp2a 14127 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((10 โˆˆ โ„ โˆง 27 โˆˆ โ„ค โˆง 30 โˆˆ โ„ค) โˆง (1 < 10 โˆง 27 < 30)) โ†’ (10โ†‘27) < (10โ†‘30))
5141, 49, 50mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (10โ†‘27) < (10โ†‘30)
5238, 51pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 โ‰ค (10โ†‘27) โˆง (10โ†‘27) < (10โ†‘30))
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (0 โ‰ค (10โ†‘27) โˆง (10โ†‘27) < (10โ†‘30)))
54 ltmul12a 12066 . . . . . . . . . . . . . . . . . . . . . . 23 ((((1 โˆˆ โ„ โˆง 8 โˆˆ โ„) โˆง (0 โ‰ค 1 โˆง 1 < 8)) โˆง (((10โ†‘27) โˆˆ โ„ โˆง (10โ†‘30) โˆˆ โ„) โˆง (0 โ‰ค (10โ†‘27) โˆง (10โ†‘27) < (10โ†‘30)))) โ†’ (1 ยท (10โ†‘27)) < (8 ยท (10โ†‘30)))
5524, 28, 35, 53, 54syl22anc 837 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (1 ยท (10โ†‘27)) < (8 ยท (10โ†‘30)))
5620, 55eqbrtrrid 5183 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (10โ†‘27) < (8 ยท (10โ†‘30)))
579a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (10โ†‘27) โˆˆ โ„)
5822, 33remulcli 11226 . . . . . . . . . . . . . . . . . . . . . . 23 (8 ยท (10โ†‘30)) โˆˆ โ„
5958a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (8 ยท (10โ†‘30)) โˆˆ โ„)
60 nnre 12215 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘š โˆˆ โ„• โ†’ ๐‘š โˆˆ โ„)
6160adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ ๐‘š โˆˆ โ„)
62 lttr 11286 . . . . . . . . . . . . . . . . . . . . . 22 (((10โ†‘27) โˆˆ โ„ โˆง (8 ยท (10โ†‘30)) โˆˆ โ„ โˆง ๐‘š โˆˆ โ„) โ†’ (((10โ†‘27) < (8 ยท (10โ†‘30)) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โ†’ (10โ†‘27) < ๐‘š))
6357, 59, 61, 62syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (((10โ†‘27) < (8 ยท (10โ†‘30)) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โ†’ (10โ†‘27) < ๐‘š))
6456, 63mpand 693 . . . . . . . . . . . . . . . . . . . 20 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ ((8 ยท (10โ†‘30)) < ๐‘š โ†’ (10โ†‘27) < ๐‘š))
6564imp 407 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โ†’ (10โ†‘27) < ๐‘š)
662adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„)
6766, 57, 613jca 1128 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ (๐‘› โˆˆ โ„ โˆง (10โ†‘27) โˆˆ โ„ โˆง ๐‘š โˆˆ โ„))
6867adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โ†’ (๐‘› โˆˆ โ„ โˆง (10โ†‘27) โˆˆ โ„ โˆง ๐‘š โˆˆ โ„))
69 lelttr 11300 . . . . . . . . . . . . . . . . . . . 20 ((๐‘› โˆˆ โ„ โˆง (10โ†‘27) โˆˆ โ„ โˆง ๐‘š โˆˆ โ„) โ†’ ((๐‘› โ‰ค (10โ†‘27) โˆง (10โ†‘27) < ๐‘š) โ†’ ๐‘› < ๐‘š))
7068, 69syl 17 . . . . . . . . . . . . . . . . . . 19 (((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โ†’ ((๐‘› โ‰ค (10โ†‘27) โˆง (10โ†‘27) < ๐‘š) โ†’ ๐‘› < ๐‘š))
7165, 70mpan2d 692 . . . . . . . . . . . . . . . . . 18 (((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ ๐‘› < ๐‘š))
7271imp 407 . . . . . . . . . . . . . . . . 17 ((((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โˆง ๐‘› โ‰ค (10โ†‘27)) โ†’ ๐‘› < ๐‘š)
7372anim1i 615 . . . . . . . . . . . . . . . 16 (((((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โˆง ๐‘› โ‰ค (10โ†‘27)) โˆง 7 < ๐‘›) โ†’ (๐‘› < ๐‘š โˆง 7 < ๐‘›))
7473ancomd 462 . . . . . . . . . . . . . . 15 (((((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โˆง ๐‘› โ‰ค (10โ†‘27)) โˆง 7 < ๐‘›) โ†’ (7 < ๐‘› โˆง ๐‘› < ๐‘š))
75 pm2.27 42 . . . . . . . . . . . . . . 15 ((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ (((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ๐‘› โˆˆ GoldbachOdd ))
7674, 75syl 17 . . . . . . . . . . . . . 14 (((((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โˆง ๐‘› โ‰ค (10โ†‘27)) โˆง 7 < ๐‘›) โ†’ (((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ๐‘› โˆˆ GoldbachOdd ))
7776ex 413 . . . . . . . . . . . . 13 ((((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โˆง ๐‘› โ‰ค (10โ†‘27)) โ†’ (7 < ๐‘› โ†’ (((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ๐‘› โˆˆ GoldbachOdd )))
7877com23 86 . . . . . . . . . . . 12 ((((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โˆง (8 ยท (10โ†‘30)) < ๐‘š) โˆง ๐‘› โ‰ค (10โ†‘27)) โ†’ (((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))
7978exp41 435 . . . . . . . . . . 11 (๐‘› โˆˆ Odd โ†’ (๐‘š โˆˆ โ„• โ†’ ((8 ยท (10โ†‘30)) < ๐‘š โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ (((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))))
8079com25 99 . . . . . . . . . 10 (๐‘› โˆˆ Odd โ†’ (((7 < ๐‘› โˆง ๐‘› < ๐‘š) โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ((8 ยท (10โ†‘30)) < ๐‘š โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ (๐‘š โˆˆ โ„• โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))))
8118, 80syld 47 . . . . . . . . 9 (๐‘› โˆˆ Odd โ†’ (โˆ€๐‘œ โˆˆ Odd ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†’ ((8 ยท (10โ†‘30)) < ๐‘š โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ (๐‘š โˆˆ โ„• โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))))
8281com15 101 . . . . . . . 8 (๐‘š โˆˆ โ„• โ†’ (โˆ€๐‘œ โˆˆ Odd ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†’ ((8 ยท (10โ†‘30)) < ๐‘š โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))))
8382com23 86 . . . . . . 7 (๐‘š โˆˆ โ„• โ†’ ((8 ยท (10โ†‘30)) < ๐‘š โ†’ (โˆ€๐‘œ โˆˆ Odd ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))))
8483imp32 419 . . . . . 6 ((๐‘š โˆˆ โ„• โˆง ((8 ยท (10โ†‘30)) < ๐‘š โˆง โˆ€๐‘œ โˆˆ Odd ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd ))) โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))
8584rexlimiva 3147 . . . . 5 (โˆƒ๐‘š โˆˆ โ„• ((8 ยท (10โ†‘30)) < ๐‘š โˆง โˆ€๐‘œ โˆˆ Odd ((7 < ๐‘œ โˆง ๐‘œ < ๐‘š) โ†’ ๐‘œ โˆˆ GoldbachOdd )) โ†’ (๐‘› โ‰ค (10โ†‘27) โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))
8612, 85ax-mp 5 . . . 4 (๐‘› โ‰ค (10โ†‘27) โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))
87 tgoldbachgtALTV 46466 . . . . 5 โˆƒ๐‘š โˆˆ โ„• (๐‘š โ‰ค (10โ†‘27) โˆง โˆ€๐‘œ โˆˆ Odd (๐‘š < ๐‘œ โ†’ ๐‘œ โˆˆ GoldbachOdd ))
88 breq2 5151 . . . . . . . . . . 11 (๐‘œ = ๐‘› โ†’ (๐‘š < ๐‘œ โ†” ๐‘š < ๐‘›))
8988, 16imbi12d 344 . . . . . . . . . 10 (๐‘œ = ๐‘› โ†’ ((๐‘š < ๐‘œ โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†” (๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))
9089rspcv 3608 . . . . . . . . 9 (๐‘› โˆˆ Odd โ†’ (โˆ€๐‘œ โˆˆ Odd (๐‘š < ๐‘œ โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†’ (๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))
91 lelttr 11300 . . . . . . . . . . . . . . . . . . . 20 ((๐‘š โˆˆ โ„ โˆง (10โ†‘27) โˆˆ โ„ โˆง ๐‘› โˆˆ โ„) โ†’ ((๐‘š โ‰ค (10โ†‘27) โˆง (10โ†‘27) < ๐‘›) โ†’ ๐‘š < ๐‘›))
9261, 57, 66, 91syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ ((๐‘š โ‰ค (10โ†‘27) โˆง (10โ†‘27) < ๐‘›) โ†’ ๐‘š < ๐‘›))
9392expcomd 417 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ Odd โˆง ๐‘š โˆˆ โ„•) โ†’ ((10โ†‘27) < ๐‘› โ†’ (๐‘š โ‰ค (10โ†‘27) โ†’ ๐‘š < ๐‘›)))
9493ex 413 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ Odd โ†’ (๐‘š โˆˆ โ„• โ†’ ((10โ†‘27) < ๐‘› โ†’ (๐‘š โ‰ค (10โ†‘27) โ†’ ๐‘š < ๐‘›))))
9594com23 86 . . . . . . . . . . . . . . . 16 (๐‘› โˆˆ Odd โ†’ ((10โ†‘27) < ๐‘› โ†’ (๐‘š โˆˆ โ„• โ†’ (๐‘š โ‰ค (10โ†‘27) โ†’ ๐‘š < ๐‘›))))
9695imp43 428 . . . . . . . . . . . . . . 15 (((๐‘› โˆˆ Odd โˆง (10โ†‘27) < ๐‘›) โˆง (๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27))) โ†’ ๐‘š < ๐‘›)
97 pm2.27 42 . . . . . . . . . . . . . . 15 (๐‘š < ๐‘› โ†’ ((๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ๐‘› โˆˆ GoldbachOdd ))
9896, 97syl 17 . . . . . . . . . . . . . 14 (((๐‘› โˆˆ Odd โˆง (10โ†‘27) < ๐‘›) โˆง (๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27))) โ†’ ((๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ๐‘› โˆˆ GoldbachOdd ))
9998a1dd 50 . . . . . . . . . . . . 13 (((๐‘› โˆˆ Odd โˆง (10โ†‘27) < ๐‘›) โˆง (๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27))) โ†’ ((๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))
10099ex 413 . . . . . . . . . . . 12 ((๐‘› โˆˆ Odd โˆง (10โ†‘27) < ๐‘›) โ†’ ((๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27)) โ†’ ((๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))
101100com23 86 . . . . . . . . . . 11 ((๐‘› โˆˆ Odd โˆง (10โ†‘27) < ๐‘›) โ†’ ((๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ((๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27)) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))
102101ex 413 . . . . . . . . . 10 (๐‘› โˆˆ Odd โ†’ ((10โ†‘27) < ๐‘› โ†’ ((๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ((๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27)) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))))
103102com23 86 . . . . . . . . 9 (๐‘› โˆˆ Odd โ†’ ((๐‘š < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ) โ†’ ((10โ†‘27) < ๐‘› โ†’ ((๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27)) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))))
10490, 103syld 47 . . . . . . . 8 (๐‘› โˆˆ Odd โ†’ (โˆ€๐‘œ โˆˆ Odd (๐‘š < ๐‘œ โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†’ ((10โ†‘27) < ๐‘› โ†’ ((๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27)) โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))))
105104com14 96 . . . . . . 7 ((๐‘š โˆˆ โ„• โˆง ๐‘š โ‰ค (10โ†‘27)) โ†’ (โˆ€๐‘œ โˆˆ Odd (๐‘š < ๐‘œ โ†’ ๐‘œ โˆˆ GoldbachOdd ) โ†’ ((10โ†‘27) < ๐‘› โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))))
106105impr 455 . . . . . 6 ((๐‘š โˆˆ โ„• โˆง (๐‘š โ‰ค (10โ†‘27) โˆง โˆ€๐‘œ โˆˆ Odd (๐‘š < ๐‘œ โ†’ ๐‘œ โˆˆ GoldbachOdd ))) โ†’ ((10โ†‘27) < ๐‘› โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))
107106rexlimiva 3147 . . . . 5 (โˆƒ๐‘š โˆˆ โ„• (๐‘š โ‰ค (10โ†‘27) โˆง โˆ€๐‘œ โˆˆ Odd (๐‘š < ๐‘œ โ†’ ๐‘œ โˆˆ GoldbachOdd )) โ†’ ((10โ†‘27) < ๐‘› โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))))
10887, 107ax-mp 5 . . . 4 ((10โ†‘27) < ๐‘› โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))
10986, 108jaoi 855 . . 3 ((๐‘› โ‰ค (10โ†‘27) โˆจ (10โ†‘27) < ๐‘›) โ†’ (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )))
11011, 109mpcom 38 . 2 (๐‘› โˆˆ Odd โ†’ (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd ))
111110rgen 3063 1 โˆ€๐‘› โˆˆ Odd (7 < ๐‘› โ†’ ๐‘› โˆˆ GoldbachOdd )
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3061  โˆƒwrex 3070   class class class wbr 5147  (class class class)co 7405  โ„cr 11105  0cc0 11106  1c1 11107   ยท cmul 11111   < clt 11244   โ‰ค cle 11245  โ„•cn 12208  2c2 12263  3c3 12264  7c7 12268  8c8 12269  โ„•0cn0 12468  โ„คcz 12554  cdc 12673  โ†‘cexp 14023   Odd codd 46279   GoldbachOdd cgbo 46401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-bgbltosilva 46464  ax-tgoldbachgt 46465  ax-hgprmladder 46468
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-rp 12971  df-ico 13326  df-fz 13481  df-fzo 13624  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-dvds 16194  df-prm 16605  df-iccp 46068  df-even 46280  df-odd 46281  df-gbe 46402  df-gbo 46404
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator