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

Theorem tgoldbachOLD 42139
Description: Obsolete version of tgoldbach 42132 as of 9-Sep-2021. (Contributed by AV, 2-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
tgoldbachOLD 𝑛 ∈ Odd (7 < 𝑛𝑛 ∈ GoldbachOdd )

Proof of Theorem tgoldbachOLD
Dummy variables 𝑚 𝑜 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oddz 41971 . . . . 5 (𝑛 ∈ Odd → 𝑛 ∈ ℤ)
21zred 11595 . . . 4 (𝑛 ∈ Odd → 𝑛 ∈ ℝ)
3 10reOLD 11222 . . . . 5 10 ∈ ℝ
4 2nn0 11422 . . . . . . 7 2 ∈ ℕ0
5 7nn 11303 . . . . . . 7 7 ∈ ℕ
64, 5decnncl 11631 . . . . . 6 27 ∈ ℕ
76nnnn0i 11413 . . . . 5 27 ∈ ℕ0
8 reexpcl 12992 . . . . 5 ((10 ∈ ℝ ∧ 27 ∈ ℕ0) → (10↑27) ∈ ℝ)
93, 7, 8mp2an 710 . . . 4 (10↑27) ∈ ℝ
10 lelttric 10257 . . . 4 ((𝑛 ∈ ℝ ∧ (10↑27) ∈ ℝ) → (𝑛 ≤ (10↑27) ∨ (10↑27) < 𝑛))
112, 9, 10sylancl 697 . . 3 (𝑛 ∈ Odd → (𝑛 ≤ (10↑27) ∨ (10↑27) < 𝑛))
12 tgoldbachltOLD 42137 . . . . 5 𝑚 ∈ ℕ ((8 · (10↑30)) < 𝑚 ∧ ∀𝑜 ∈ Odd ((7 < 𝑜𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ))
13 breq2 4764 . . . . . . . . . . . . 13 (𝑜 = 𝑛 → (7 < 𝑜 ↔ 7 < 𝑛))
14 breq1 4763 . . . . . . . . . . . . 13 (𝑜 = 𝑛 → (𝑜 < 𝑚𝑛 < 𝑚))
1513, 14anbi12d 749 . . . . . . . . . . . 12 (𝑜 = 𝑛 → ((7 < 𝑜𝑜 < 𝑚) ↔ (7 < 𝑛𝑛 < 𝑚)))
16 eleq1 2791 . . . . . . . . . . . 12 (𝑜 = 𝑛 → (𝑜 ∈ GoldbachOdd ↔ 𝑛 ∈ GoldbachOdd ))
1715, 16imbi12d 333 . . . . . . . . . . 11 (𝑜 = 𝑛 → (((7 < 𝑜𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ) ↔ ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )))
1817rspcv 3409 . . . . . . . . . 10 (𝑛 ∈ Odd → (∀𝑜 ∈ Odd ((7 < 𝑜𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ) → ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )))
199recni 10165 . . . . . . . . . . . . . . . . . . . . . . 23 (10↑27) ∈ ℂ
2019mulid2i 10156 . . . . . . . . . . . . . . . . . . . . . 22 (1 · (10↑27)) = (10↑27)
21 1re 10152 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ
22 8re 11218 . . . . . . . . . . . . . . . . . . . . . . . . 25 8 ∈ ℝ
2321, 22pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℝ ∧ 8 ∈ ℝ)
2423a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (1 ∈ ℝ ∧ 8 ∈ ℝ))
25 0le1 10664 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ 1
26 1lt8 11334 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 < 8
2725, 26pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ≤ 1 ∧ 1 < 8)
2827a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (0 ≤ 1 ∧ 1 < 8))
29 3nn 11299 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 ∈ ℕ
3029decnncl2 11638 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 30 ∈ ℕ
3130nnnn0i 11413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 30 ∈ ℕ0
32 reexpcl 12992 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((10 ∈ ℝ ∧ 30 ∈ ℕ0) → (10↑30) ∈ ℝ)
333, 31, 32mp2an 710 . . . . . . . . . . . . . . . . . . . . . . . . 25 (10↑30) ∈ ℝ
349, 33pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . 24 ((10↑27) ∈ ℝ ∧ (10↑30) ∈ ℝ)
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((10↑27) ∈ ℝ ∧ (10↑30) ∈ ℝ))
36 10nn0OLD 11430 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 10 ∈ ℕ0
3736, 7nn0expcli 13001 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (10↑27) ∈ ℕ0
3837nn0ge0i 11433 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ≤ (10↑27)
396nnzi 11514 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 27 ∈ ℤ
4030nnzi 11514 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 30 ∈ ℤ
413, 39, 403pm3.2i 1376 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (10 ∈ ℝ ∧ 27 ∈ ℤ ∧ 30 ∈ ℤ)
42 1lt10OLD 11351 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 < 10
43 3nn0 11423 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 ∈ ℕ0
44 7nn0 11427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 7 ∈ ℕ0
45 0nn0 11420 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ∈ ℕ0
46 7lt10OLD 11345 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 7 < 10
47 2lt3 11308 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 < 3
484, 43, 44, 45, 46, 47decltcOLD 11646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 27 < 30
4942, 48pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 < 10 ∧ 27 < 30)
50 ltexp2a 13027 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((10 ∈ ℝ ∧ 27 ∈ ℤ ∧ 30 ∈ ℤ) ∧ (1 < 10 ∧ 27 < 30)) → (10↑27) < (10↑30))
5141, 49, 50mp2an 710 . . . . . . . . . . . . . . . . . . . . . . . . 25 (10↑27) < (10↑30)
5238, 51pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 ≤ (10↑27) ∧ (10↑27) < (10↑30))
5352a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (0 ≤ (10↑27) ∧ (10↑27) < (10↑30)))
54 ltmul12a 10992 . . . . . . . . . . . . . . . . . . . . . . 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 1440 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (1 · (10↑27)) < (8 · (10↑30)))
5620, 55syl5eqbrr 4796 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (10↑27) < (8 · (10↑30)))
579a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (10↑27) ∈ ℝ)
5822, 33remulcli 10167 . . . . . . . . . . . . . . . . . . . . . . 23 (8 · (10↑30)) ∈ ℝ
5958a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (8 · (10↑30)) ∈ ℝ)
60 nnre 11140 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
6160adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
62 lttr 10227 . . . . . . . . . . . . . . . . . . . . . 22 (((10↑27) ∈ ℝ ∧ (8 · (10↑30)) ∈ ℝ ∧ 𝑚 ∈ ℝ) → (((10↑27) < (8 · (10↑30)) ∧ (8 · (10↑30)) < 𝑚) → (10↑27) < 𝑚))
6357, 59, 61, 62syl3anc 1439 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (((10↑27) < (8 · (10↑30)) ∧ (8 · (10↑30)) < 𝑚) → (10↑27) < 𝑚))
6456, 63mpand 713 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((8 · (10↑30)) < 𝑚 → (10↑27) < 𝑚))
6564imp 444 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8 · (10↑30)) < 𝑚) → (10↑27) < 𝑚)
662adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℝ)
6766, 57, 613jca 1379 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → (𝑛 ∈ ℝ ∧ (10↑27) ∈ ℝ ∧ 𝑚 ∈ ℝ))
6867adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8 · (10↑30)) < 𝑚) → (𝑛 ∈ ℝ ∧ (10↑27) ∈ ℝ ∧ 𝑚 ∈ ℝ))
69 lelttr 10241 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℝ ∧ (10↑27) ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑛 ≤ (10↑27) ∧ (10↑27) < 𝑚) → 𝑛 < 𝑚))
7068, 69syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8 · (10↑30)) < 𝑚) → ((𝑛 ≤ (10↑27) ∧ (10↑27) < 𝑚) → 𝑛 < 𝑚))
7165, 70mpan2d 712 . . . . . . . . . . . . . . . . . 18 (((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8 · (10↑30)) < 𝑚) → (𝑛 ≤ (10↑27) → 𝑛 < 𝑚))
7271imp 444 . . . . . . . . . . . . . . . . 17 ((((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8 · (10↑30)) < 𝑚) ∧ 𝑛 ≤ (10↑27)) → 𝑛 < 𝑚)
7372anim1i 593 . . . . . . . . . . . . . . . 16 (((((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) ∧ (8 · (10↑30)) < 𝑚) ∧ 𝑛 ≤ (10↑27)) ∧ 7 < 𝑛) → (𝑛 < 𝑚 ∧ 7 < 𝑛))
7473ancomd 466 . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . . 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 639 . . . . . . . . . . 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 448 . . . . . 6 ((𝑚 ∈ ℕ ∧ ((8 · (10↑30)) < 𝑚 ∧ ∀𝑜 ∈ Odd ((7 < 𝑜𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd ))) → (𝑛 ≤ (10↑27) → (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd ))))
8584rexlimiva 3130 . . . . 5 (∃𝑚 ∈ ℕ ((8 · (10↑30)) < 𝑚 ∧ ∀𝑜 ∈ Odd ((7 < 𝑜𝑜 < 𝑚) → 𝑜 ∈ GoldbachOdd )) → (𝑛 ≤ (10↑27) → (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd ))))
8612, 85ax-mp 5 . . . 4 (𝑛 ≤ (10↑27) → (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd )))
87 ax-tgoldbachgtOLD 42138 . . . . 5 𝑚 ∈ ℕ (𝑚 ≤ (10↑27) ∧ ∀𝑜 ∈ Odd (𝑚 < 𝑜𝑜 ∈ GoldbachOdd ))
88 breq2 4764 . . . . . . . . . . 11 (𝑜 = 𝑛 → (𝑚 < 𝑜𝑚 < 𝑛))
8988, 16imbi12d 333 . . . . . . . . . 10 (𝑜 = 𝑛 → ((𝑚 < 𝑜𝑜 ∈ GoldbachOdd ) ↔ (𝑚 < 𝑛𝑛 ∈ GoldbachOdd )))
9089rspcv 3409 . . . . . . . . 9 (𝑛 ∈ Odd → (∀𝑜 ∈ Odd (𝑚 < 𝑜𝑜 ∈ GoldbachOdd ) → (𝑚 < 𝑛𝑛 ∈ GoldbachOdd )))
91 lelttr 10241 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ ℝ ∧ (10↑27) ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((𝑚 ≤ (10↑27) ∧ (10↑27) < 𝑛) → 𝑚 < 𝑛))
9261, 57, 66, 91syl3anc 1439 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((𝑚 ≤ (10↑27) ∧ (10↑27) < 𝑛) → 𝑚 < 𝑛))
9392expcomd 453 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ Odd ∧ 𝑚 ∈ ℕ) → ((10↑27) < 𝑛 → (𝑚 ≤ (10↑27) → 𝑚 < 𝑛)))
9493ex 449 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ Odd → (𝑚 ∈ ℕ → ((10↑27) < 𝑛 → (𝑚 ≤ (10↑27) → 𝑚 < 𝑛))))
9594com23 86 . . . . . . . . . . . . . . . 16 (𝑛 ∈ Odd → ((10↑27) < 𝑛 → (𝑚 ∈ ℕ → (𝑚 ≤ (10↑27) → 𝑚 < 𝑛))))
9695imp43 622 . . . . . . . . . . . . . . 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 449 . . . . . . . . . . . 12 ((𝑛 ∈ Odd ∧ (10↑27) < 𝑛) → ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (10↑27)) → ((𝑚 < 𝑛𝑛 ∈ GoldbachOdd ) → (7 < 𝑛𝑛 ∈ GoldbachOdd ))))
101100com23 86 . . . . . . . . . . 11 ((𝑛 ∈ Odd ∧ (10↑27) < 𝑛) → ((𝑚 < 𝑛𝑛 ∈ GoldbachOdd ) → ((𝑚 ∈ ℕ ∧ 𝑚 ≤ (10↑27)) → (7 < 𝑛𝑛 ∈ GoldbachOdd ))))
102101ex 449 . . . . . . . . . 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 650 . . . . . 6 ((𝑚 ∈ ℕ ∧ (𝑚 ≤ (10↑27) ∧ ∀𝑜 ∈ Odd (𝑚 < 𝑜𝑜 ∈ GoldbachOdd ))) → ((10↑27) < 𝑛 → (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd ))))
107106rexlimiva 3130 . . . . 5 (∃𝑚 ∈ ℕ (𝑚 ≤ (10↑27) ∧ ∀𝑜 ∈ Odd (𝑚 < 𝑜𝑜 ∈ GoldbachOdd )) → ((10↑27) < 𝑛 → (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd ))))
10887, 107ax-mp 5 . . . 4 ((10↑27) < 𝑛 → (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd )))
10986, 108jaoi 393 . . 3 ((𝑛 ≤ (10↑27) ∨ (10↑27) < 𝑛) → (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd )))
11011, 109mpcom 38 . 2 (𝑛 ∈ Odd → (7 < 𝑛𝑛 ∈ GoldbachOdd ))
111110rgen 3024 1 𝑛 ∈ Odd (7 < 𝑛𝑛 ∈ GoldbachOdd )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383  w3a 1072  wcel 2103  wral 3014  wrex 3015   class class class wbr 4760  (class class class)co 6765  cr 10048  0cc0 10049  1c1 10050   · cmul 10054   < clt 10187  cle 10188  cn 11133  2c2 11183  3c3 11184  7c7 11188  8c8 11189  10c10 11191  0cn0 11405  cz 11490  cdc 11606  cexp 12975   Odd codd 41965   GoldbachOdd cgbo 42062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127  ax-bgbltosilvaOLD 42133  ax-hgprmladderOLD 42135  ax-tgoldbachgtOLD 42138
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-fal 1602  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-sup 8464  df-inf 8465  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-10OLD 11200  df-n0 11406  df-z 11491  df-dec 11607  df-uz 11801  df-rp 11947  df-ico 12295  df-fz 12441  df-fzo 12581  df-seq 12917  df-exp 12976  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-dvds 15104  df-prm 15509  df-iccp 41777  df-even 41966  df-odd 41967  df-gbe 42063  df-gbo 42065
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator