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

Theorem tgoldbachltOLD 41019
 Description: Obsolete version of tgoldbachlt 41012 as of 9-Sep-2021. (Contributed by AV, 4-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
tgoldbachltOLD 𝑚 ∈ ℕ ((8 · (10↑30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV ))
Distinct variable group:   𝑚,𝑛

Proof of Theorem tgoldbachltOLD
StepHypRef Expression
1 8nn0 11266 . . . 4 8 ∈ ℕ0
2 8nn 11142 . . . 4 8 ∈ ℕ
31, 2decnncl 11469 . . 3 88 ∈ ℕ
4 10nnOLD 11144 . . . 4 10 ∈ ℕ
5 2nn0 11260 . . . . 5 2 ∈ ℕ0
6 9nn0 11267 . . . . 5 9 ∈ ℕ0
75, 6deccl 11463 . . . 4 29 ∈ ℕ0
8 nnexpcl 12820 . . . 4 ((10 ∈ ℕ ∧ 29 ∈ ℕ0) → (10↑29) ∈ ℕ)
94, 7, 8mp2an 707 . . 3 (10↑29) ∈ ℕ
103, 9nnmulcli 10995 . 2 (88 · (10↑29)) ∈ ℕ
11 id 22 . . 3 ((88 · (10↑29)) ∈ ℕ → (88 · (10↑29)) ∈ ℕ)
12 breq2 4622 . . . . 5 (𝑚 = (88 · (10↑29)) → ((8 · (10↑30)) < 𝑚 ↔ (8 · (10↑30)) < (88 · (10↑29))))
13 breq2 4622 . . . . . . . 8 (𝑚 = (88 · (10↑29)) → (𝑛 < 𝑚𝑛 < (88 · (10↑29))))
1413anbi2d 739 . . . . . . 7 (𝑚 = (88 · (10↑29)) → ((7 < 𝑛𝑛 < 𝑚) ↔ (7 < 𝑛𝑛 < (88 · (10↑29)))))
1514imbi1d 331 . . . . . 6 (𝑚 = (88 · (10↑29)) → (((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV ) ↔ ((7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV )))
1615ralbidv 2981 . . . . 5 (𝑚 = (88 · (10↑29)) → (∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV ) ↔ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV )))
1712, 16anbi12d 746 . . . 4 (𝑚 = (88 · (10↑29)) → (((8 · (10↑30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV )) ↔ ((8 · (10↑30)) < (88 · (10↑29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV ))))
1817adantl 482 . . 3 (((88 · (10↑29)) ∈ ℕ ∧ 𝑚 = (88 · (10↑29))) → (((8 · (10↑30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV )) ↔ ((8 · (10↑30)) < (88 · (10↑29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV ))))
19 simplr 791 . . . . . . 7 ((((88 · (10↑29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛𝑛 < (88 · (10↑29)))) → 𝑛 ∈ Odd )
20 simprl 793 . . . . . . 7 ((((88 · (10↑29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛𝑛 < (88 · (10↑29)))) → 7 < 𝑛)
21 simprr 795 . . . . . . 7 ((((88 · (10↑29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛𝑛 < (88 · (10↑29)))) → 𝑛 < (88 · (10↑29)))
22 tgblthelfgottOLD 41018 . . . . . . 7 ((𝑛 ∈ Odd ∧ 7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV )
2319, 20, 21, 22syl3anc 1323 . . . . . 6 ((((88 · (10↑29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) ∧ (7 < 𝑛𝑛 < (88 · (10↑29)))) → 𝑛 ∈ GoldbachOddALTV )
2423ex 450 . . . . 5 (((88 · (10↑29)) ∈ ℕ ∧ 𝑛 ∈ Odd ) → ((7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV ))
2524ralrimiva 2961 . . . 4 ((88 · (10↑29)) ∈ ℕ → ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV ))
262, 9nnmulcli 10995 . . . . . . 7 (8 · (10↑29)) ∈ ℕ
2726nngt0i 11005 . . . . . 6 0 < (8 · (10↑29))
2826nnrei 10980 . . . . . . 7 (8 · (10↑29)) ∈ ℝ
29 3nn0 11261 . . . . . . . . . . 11 3 ∈ ℕ0
30 0nn0 11258 . . . . . . . . . . 11 0 ∈ ℕ0
3129, 30deccl 11463 . . . . . . . . . 10 30 ∈ ℕ0
32 nnexpcl 12820 . . . . . . . . . 10 ((10 ∈ ℕ ∧ 30 ∈ ℕ0) → (10↑30) ∈ ℕ)
334, 31, 32mp2an 707 . . . . . . . . 9 (10↑30) ∈ ℕ
342, 33nnmulcli 10995 . . . . . . . 8 (8 · (10↑30)) ∈ ℕ
3534nnrei 10980 . . . . . . 7 (8 · (10↑30)) ∈ ℝ
3628, 35ltaddposi 10528 . . . . . 6 (0 < (8 · (10↑29)) ↔ (8 · (10↑30)) < ((8 · (10↑30)) + (8 · (10↑29))))
3727, 36mpbi 220 . . . . 5 (8 · (10↑30)) < ((8 · (10↑30)) + (8 · (10↑29)))
38 dfdecOLD 11446 . . . . . . 7 88 = ((10 · 8) + 8)
3938oveq1i 6620 . . . . . 6 (88 · (10↑29)) = (((10 · 8) + 8) · (10↑29))
404, 2nnmulcli 10995 . . . . . . . 8 (10 · 8) ∈ ℕ
4140nncni 10981 . . . . . . 7 (10 · 8) ∈ ℂ
42 8cn 11057 . . . . . . 7 8 ∈ ℂ
439nncni 10981 . . . . . . 7 (10↑29) ∈ ℂ
4441, 42, 43adddiri 10002 . . . . . 6 (((10 · 8) + 8) · (10↑29)) = (((10 · 8) · (10↑29)) + (8 · (10↑29)))
4541, 43mulcomi 9997 . . . . . . . . 9 ((10 · 8) · (10↑29)) = ((10↑29) · (10 · 8))
464nncni 10981 . . . . . . . . . 10 10 ∈ ℂ
4743, 46, 42mulassi 10000 . . . . . . . . 9 (((10↑29) · 10) · 8) = ((10↑29) · (10 · 8))
48 nncn 10979 . . . . . . . . . . . . 13 (10 ∈ ℕ → 10 ∈ ℂ)
497a1i 11 . . . . . . . . . . . . 13 (10 ∈ ℕ → 29 ∈ ℕ0)
5048, 49expp1d 12956 . . . . . . . . . . . 12 (10 ∈ ℕ → (10↑(29 + 1)) = ((10↑29) · 10))
514, 50ax-mp 5 . . . . . . . . . . 11 (10↑(29 + 1)) = ((10↑29) · 10)
5251eqcomi 2630 . . . . . . . . . 10 ((10↑29) · 10) = (10↑(29 + 1))
5352oveq1i 6620 . . . . . . . . 9 (((10↑29) · 10) · 8) = ((10↑(29 + 1)) · 8)
5445, 47, 533eqtr2i 2649 . . . . . . . 8 ((10 · 8) · (10↑29)) = ((10↑(29 + 1)) · 8)
5554oveq1i 6620 . . . . . . 7 (((10 · 8) · (10↑29)) + (8 · (10↑29))) = (((10↑(29 + 1)) · 8) + (8 · (10↑29)))
56 2p1e3 11102 . . . . . . . . . . 11 (2 + 1) = 3
57 eqid 2621 . . . . . . . . . . 11 29 = 29
585, 56, 57decsucc 11501 . . . . . . . . . 10 (29 + 1) = 30
5958oveq2i 6621 . . . . . . . . 9 (10↑(29 + 1)) = (10↑30)
6059oveq1i 6620 . . . . . . . 8 ((10↑(29 + 1)) · 8) = ((10↑30) · 8)
6160oveq1i 6620 . . . . . . 7 (((10↑(29 + 1)) · 8) + (8 · (10↑29))) = (((10↑30) · 8) + (8 · (10↑29)))
6233nncni 10981 . . . . . . . 8 (10↑30) ∈ ℂ
63 mulcom 9973 . . . . . . . . 9 (((10↑30) ∈ ℂ ∧ 8 ∈ ℂ) → ((10↑30) · 8) = (8 · (10↑30)))
6463oveq1d 6625 . . . . . . . 8 (((10↑30) ∈ ℂ ∧ 8 ∈ ℂ) → (((10↑30) · 8) + (8 · (10↑29))) = ((8 · (10↑30)) + (8 · (10↑29))))
6562, 42, 64mp2an 707 . . . . . . 7 (((10↑30) · 8) + (8 · (10↑29))) = ((8 · (10↑30)) + (8 · (10↑29)))
6655, 61, 653eqtri 2647 . . . . . 6 (((10 · 8) · (10↑29)) + (8 · (10↑29))) = ((8 · (10↑30)) + (8 · (10↑29)))
6739, 44, 663eqtri 2647 . . . . 5 (88 · (10↑29)) = ((8 · (10↑30)) + (8 · (10↑29)))
6837, 67breqtrri 4645 . . . 4 (8 · (10↑30)) < (88 · (10↑29))
6925, 68jctil 559 . . 3 ((88 · (10↑29)) ∈ ℕ → ((8 · (10↑30)) < (88 · (10↑29)) ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < (88 · (10↑29))) → 𝑛 ∈ GoldbachOddALTV )))
7011, 18, 69rspcedvd 3305 . 2 ((88 · (10↑29)) ∈ ℕ → ∃𝑚 ∈ ℕ ((8 · (10↑30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV )))
7110, 70ax-mp 5 1 𝑚 ∈ ℕ ((8 · (10↑30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛𝑛 < 𝑚) → 𝑛 ∈ GoldbachOddALTV ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908   class class class wbr 4618  (class class class)co 6610  ℂcc 9885  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892   < clt 10025  ℕcn 10971  2c2 11021  3c3 11022  7c7 11026  8c8 11027  9c9 11028  10c10 11029  ℕ0cn0 11243  ;cdc 11444  ↑cexp 12807   Odd codd 40858   GoldbachOddALTV cgboa 40951 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-bgbltosilvaOLD 41015  ax-hgprmladderOLD 41017 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-sup 8299  df-inf 8300  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-10OLD 11038  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-rp 11784  df-ico 12130  df-fz 12276  df-fzo 12414  df-seq 12749  df-exp 12808  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-dvds 14915  df-prm 15317  df-iccp 40669  df-even 40859  df-odd 40860  df-gbe 40952  df-gboa 40954 This theorem is referenced by:  tgoldbachOLD  41021
 Copyright terms: Public domain W3C validator